natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Theories of presheaf type though being geometric theories of a particular “simple” and tractable type are yet ubiquitous in the sense that every geometric theory is a quotient theory? of some theory of presheaf type.
A geometric theory is of presheaf type if its classifying topos is equivalent to a presheaf topos.
Any cartesian theory being (modulo neglectable size issues1) classified by is of presheaf type with the category of finitely presentable -models in .
More concretely, e.g. the theory of objects or the theory of intervals are of presheaf type being classified by the object classifier respectively by the topos of simplicial sets.
The inconsistent theory with axiom is of presheaf type since it is classified by the initial Grothendieck topos , the presheaf topos on the empty category.
For a category the following are equivalent:
is finitely accessible.
the category of points of some presheaf topos.
for some theory of presheaf type.
for some small category .
Cf. Beke (2004, p.923) and the references given there. In fact, these equivalences are mostly (direct consequences of) classical results in the theory of accessible categories or Grothendieck toposes.
Note that despite the above equivalences the finite accessibility of does not imply that itself is of presheaf type! One sees this already in case since there famously are non trivial (Boolean sheaf) toposes lacking points (“non empty generalized spaces without points”) yet up to Morita equivalence the only theory of presheaf type corresponding to the finite accessibility of the empty category is the inconsistent theory.
The following proposition shows in which sense theories of presheaf type are still determined by their (finitely presentable) models in :
A geometric theory is of presheaf type iff (modulo neglectable size issues)
Proof. “”:
(Cf. Caramello 2018, pp.198f)
By assumption . Since (by Johnstone 2002, p.10) we can assume that is Cauchy complete.
We have:
(by Johnstone 2002, p.723, or Caramello 2018, p.198)
(by Johnstone 2002 4.2.2.(iii), p.724)
(from Diaconescu’s theorem).
Whence and, accordingly, .
In other words, theories of presheaf type are precisely those geometric theories such that their classifying toposes can be represented as presheaf toposes .
This implies e.g. that any consistent theory of presheaf type has models in .
Tibor Beke, Theories of presheaf type , JSL 69 no.3 (2004) pp.923-934. (pdf)
Olivia Caramello, Theories, Sites, Toposes , Oxford UP 2018. (chapters 6-9)
Matthias Hutzler, Syntactic presentations for glued toposes and for crystalline toposes, Phd. diss. Universität Augsburg 2021. (arXiv:2206.11244)
Peter Johnstone, Sketches of an Elephant vols.1-2 , Oxford UP 2002.
This means here (and in the following) that the essentially small category has to be replaced by a skeleton. ↩
Last revised on April 23, 2023 at 18:25:14. See the history of this page for a list of all contributions to it.